(0) Obligation:
Clauses:
at(X, fido) :- ','(at(X, mary), near(X)).
at(ta, mary).
at(jm, mary).
near(jm).
Query: at(a,a)
(1) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
at_in: (f,f) (f,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(
x1,
x2) =
at_in_aa
U1_aa(
x1,
x2) =
U1_aa(
x2)
at_in_ag(
x1,
x2) =
at_in_ag(
x2)
fido =
fido
U1_ag(
x1,
x2) =
U1_ag(
x2)
mary =
mary
at_out_ag(
x1,
x2) =
at_out_ag(
x1,
x2)
U2_ag(
x1,
x2) =
U2_ag(
x1,
x2)
near_in_g(
x1) =
near_in_g(
x1)
jm =
jm
near_out_g(
x1) =
near_out_g(
x1)
U2_aa(
x1,
x2) =
U2_aa(
x1,
x2)
at_out_aa(
x1,
x2) =
at_out_aa(
x1,
x2)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(
x1,
x2) =
at_in_aa
U1_aa(
x1,
x2) =
U1_aa(
x2)
at_in_ag(
x1,
x2) =
at_in_ag(
x2)
fido =
fido
U1_ag(
x1,
x2) =
U1_ag(
x2)
mary =
mary
at_out_ag(
x1,
x2) =
at_out_ag(
x1,
x2)
U2_ag(
x1,
x2) =
U2_ag(
x1,
x2)
near_in_g(
x1) =
near_in_g(
x1)
jm =
jm
near_out_g(
x1) =
near_out_g(
x1)
U2_aa(
x1,
x2) =
U2_aa(
x1,
x2)
at_out_aa(
x1,
x2) =
at_out_aa(
x1,
x2)
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(
x1,
x2) =
at_in_aa
U1_aa(
x1,
x2) =
U1_aa(
x2)
at_in_ag(
x1,
x2) =
at_in_ag(
x2)
fido =
fido
U1_ag(
x1,
x2) =
U1_ag(
x2)
mary =
mary
at_out_ag(
x1,
x2) =
at_out_ag(
x1,
x2)
U2_ag(
x1,
x2) =
U2_ag(
x1,
x2)
near_in_g(
x1) =
near_in_g(
x1)
jm =
jm
near_out_g(
x1) =
near_out_g(
x1)
U2_aa(
x1,
x2) =
U2_aa(
x1,
x2)
at_out_aa(
x1,
x2) =
at_out_aa(
x1,
x2)
AT_IN_AA(
x1,
x2) =
AT_IN_AA
U1_AA(
x1,
x2) =
U1_AA(
x2)
AT_IN_AG(
x1,
x2) =
AT_IN_AG(
x2)
U1_AG(
x1,
x2) =
U1_AG(
x2)
U2_AG(
x1,
x2) =
U2_AG(
x1,
x2)
NEAR_IN_G(
x1) =
NEAR_IN_G(
x1)
U2_AA(
x1,
x2) =
U2_AA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(
x1,
x2) =
at_in_aa
U1_aa(
x1,
x2) =
U1_aa(
x2)
at_in_ag(
x1,
x2) =
at_in_ag(
x2)
fido =
fido
U1_ag(
x1,
x2) =
U1_ag(
x2)
mary =
mary
at_out_ag(
x1,
x2) =
at_out_ag(
x1,
x2)
U2_ag(
x1,
x2) =
U2_ag(
x1,
x2)
near_in_g(
x1) =
near_in_g(
x1)
jm =
jm
near_out_g(
x1) =
near_out_g(
x1)
U2_aa(
x1,
x2) =
U2_aa(
x1,
x2)
at_out_aa(
x1,
x2) =
at_out_aa(
x1,
x2)
AT_IN_AA(
x1,
x2) =
AT_IN_AA
U1_AA(
x1,
x2) =
U1_AA(
x2)
AT_IN_AG(
x1,
x2) =
AT_IN_AG(
x2)
U1_AG(
x1,
x2) =
U1_AG(
x2)
U2_AG(
x1,
x2) =
U2_AG(
x1,
x2)
NEAR_IN_G(
x1) =
NEAR_IN_G(
x1)
U2_AA(
x1,
x2) =
U2_AA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 8 less nodes.
(6) TRUE